da:k:Knd fp Type, l:IdLnk, tg:Id, T:Top. dt(l;da)(tg)?T ~ da(rcv(l,tg))?T 

latex

Definitions

Knd, t  T, x. t(x), x:A. B(x), a:A fp B(a), IdLnk, Id, Top, f(x)?z, x  dom(f), , {T}, P  Q, SQType(T), fpf-domain(f), rcv(l,tg), (x  l), dt(l;da), P  Q, P & Q, P  Q, KindDeq, IdDeq, b, Prop, x:A. B(x), , Unit, tag(k), lnk(k), a = b, if b t else f fi, isrcv(k), false, A, b, False, P  Q, True, T, A & B, outl(x), compose-fpf(a;b;f), f(x)

Lemmas

false wf, squash wf, true wf, bool cases, not functionality wrt iff, assert-eq-lnk, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, bfalse wf, compose-fpf-dom, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, iff imp equal bool, iff functionality wrt iff, member-fpf-domain, assert wf, fpf-dom wf, id-deq wf, Kind-deq wf, es-dt wf, l member wf, rcv wf, fpf-domain wf, fpf-trivial-subtype-top, bool sq, top wf, Id wf, IdLnk wf, fpf wf, Knd wf